Step of Proof: adjacent-append 11,40
Inference at * 2 2 1 1 
Iof proof for Lemma adjacent-append:



1. T : Type
2. x : T
3. y : T
4. L1 : T List
5. L2 : T List
6. 0 < ||L1||
7. 0 < ||L2||
8. x = last(L1)
9. y = hd(L2)
  x = L1[(||L1|| - 1)] 
latex
 by ((Fold `last` 0) 
CollapseTHEN (Auto)) 
latex

C.

origin